﻿namespace Ast
open System

type Location = Lexing.Position * Lexing.Position

type CoqAST =
   | CoqAST of list<Sentence> * Location
   
and Sentence = 
    | Assumption of AssumptionKeyword * list<Assume> * Location
    | Definition of Definition * Location
    | AssertionBlock of Assertion * option<Proof> * Location
    | Fixpoint of Fixpoint
    | Inductive of Inductive
    | Record of Record
    //command
    | Command of Command
    //notation
    | Notation of string * Term
    //Error
    | Error of string 

//Command Vernicular
and Command = 
    | Display of Display
    | EnvReq of EnvReq

and Display = 
    | Print of Qualid
    | PrintTerm of Qualid
    | About of Qualid
    | PrintAll

and EnvReq =
    | Check of Term
    | Eval of Identifier * Term
    | Compute of Term
    | Extraction of Term
    | RecursiveExtraction of list<Qualid>
    | PrintAssumptions of Qualid
    | PrintOpaqueDep of Qualid
    | Search of Term
    | SearchAbout of Qualid
    | SearchPattern of Term
    | SearchRewrite of Term
    | Locate of Qualid
    | Load of Identifier
    | Require of Qualid 
    | RequireImport of Qualid
    | RequireExport of Qualid

//Notations
and Notation = 
    | Notation of list<Term>



//Specif & Form
and Form = 
    | Bool of bool 
    | ULop of String * Form
    | BLop of String * Form * Form
    | ForAll of Identifier * Term * Form //Term should be type
    | Ex of Identifier * option<Specif> * Form
    | Ex2 of Identifier * option<Specif> * Form * Form
    | Eq of Term * Term * option<Specif>

and Specif = 
    | Prod of Specif * Specif
    | Sum of Specif * Specif
    | SumOr of Specif * Specif
    | SumBool of Specif * Specif
    | SigT of Identifier * Specif * Specif
    | SigT2 of Identifier * Specif * Specif * Specif
    | Sig of Identifier * Specif * Form
    | Sig2 of Identifier * Specif * Form * Form
    | Term of Term

//Records
and Record =
    | Record of Identifier * option<Binders> * option<Sort> * option<Identifier> * list<Field>

and Field = 
    | FieldType of Name * option<Binders> * Term 
    | FieldTerm of Name * option<Binders> * option<Term> * Term

//Proof
and TacticInvocation = 
    | TacticInvocation of Option<Int32> * Tactic * Location

and Tactic = 
    | TacticNoArg of Identifier
    | TatcticOneArg of Identifier * Term
    | Rename of Identifier * Identifier 

//Inductive
and Inductive = 
    | Inductive of list<IndBody>
    | CoInductive of list<IndBody>

and Ibt = 
    | Ibt of Identifier * Option<Binders> * Option<Term>

and IndBody = 
    | IndBody of Identifier * Option<Binders> * Term * list<Ibt>

//Fixpoint
and Fixpoint =
    | SFixpoint of list<FixBody>
    | SCoFixpoint of list<CoFixBody>

//Definitions
and Definition = 
    | DefAssertion of Assertion * Option<Proof>
    | DefinitionD of Identifier * Option<Binders> * Option<Term> * Term
    | Let of Identifier * Option<Binders> * Option<Term> * Term

//Assumptions
and AssumptionKeyword = 
    | Axiom 
    | Conjecture 
    | Parameter 
    | Parameters 
    | Variable 
    | Variables 
    | Hypothesis 
    | Hypotheses 

and Assume = 
    | Assume of list<Identifier> * Term

//Assertion
and AssertionKeyWord = 
    | Theorem 
    | Lemma 
    | Remark 
    | Fact 
    | Corollary 
    | Proposition 
    | Definition 
    | Example

and Assertion = 
    | Assertion of AssertionKeyWord * Identifier * Option<Binders> * Term 

and Proof =
  | Proof of list<TacticInvocation> * String * Location

//Terms
and Term =
    | Products1 of Binders * Term
    | Products2 of Term * Term
    | Abstraction of Binders * Term
    | RecFunctions of FixBodies
    | CoRecFunctions of CoFixBodies
    | LocalDefinition of Identifier * Option<Binders> * Option<Term> * Term * Term 
    | Fixpoint of FixBody * Term
    | CoFixpoint of CoFixBody * Term
    | DefByCaseAnalysis of list<Name> * Option<DepReturnType> * Term * Term
    | Branch of Term * Option<DepReturnType> * Term * Term
    | TypeCast of Term * Term
    | Application of Term * list<Arg>
    | ExplicitApplication of Qualid * list<Term>
    | InterpretationScope of Term * Identifier
    | Match of list<MatchItem> * Option<ReturnType> * list<Equation>
    | Qualid of Qualid
    | Sort of Sort
    | Integer of Int32
    | Underscore
    //Logic
    | Form of Form
    | Pair of Term * Term
    //Form
    | Bool of bool 
    | ULop of String * Term
    | BLop of String * Term * Term
    | ForAll of Identifier * Term * Term //Term should be type
    | Ex of Identifier * option<Term> * Term
    | Ex2 of Identifier * option<Term> * Term * Term
    | Eq of Term * Term * option<Term>
    //specif
    | Prod of Term * Term
    | Sum of Term * Term
    | SumOr of Term * Term
    | SumBool of Term * Term
    | SigT of Identifier * Term * Term
    | SigT2 of Identifier * Term * Term * Term
    | Sig of Identifier * Term * Term
    | Sig2 of Identifier * Term * Term * Term
    //Notation
    | Notation of Notation

and Equation = 
    Equation of list<MultiPattern> * Term

and MultiPattern = list<Pattern>

and OrPattern = list<Pattern>

and Pattern = 
    | PatternList of Qualid * list<Pattern>
    | PatternIdent of Pattern * Identifier
    | Underscore 
    | Integer of Int32
    | OrPattern of list<OrPattern>
   
and MatchItem =
    | MatchItem of Term * Option<Name> * Option<Term>

and Name = 
    | Identifier of Identifier
    | Underscore

and Binder =   
    | Binder of list<Name> * Option<Term> * Option<Term>

and Arg = 
    | Term of Term
    | ExplicitTerm of Identifier * Term

and Sort =
    | Prop
    | Set
    | Type
    
and FixBody = Identifier * Binders * Option<Annotation> * Option<Term> * Term
and CoFixBody = Identifier * Option<Binders> * Option<Term> * Term

and FixBodies = 
    | FixBodie of FixBody 
    | FixBodies of list<FixBody>  * Option<Identifier>
and CoFixBodies = 
    | CoFixBodie of CoFixBody 
    | CoFixBodies of list<CoFixBody>  * Option<Identifier>

and DepReturnType = Option<Name> * ReturnType

and ReturnType = Term

and Annotation = Identifier

and Binders = list<Binder>

and Identifier = String * Location

and Qualid = list<String> * Location

//and AccessIdentifier = String * Location




